COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	reiter[w84,jmc]		A proof for Reiter
C00003 00003	Here is an EKL proof that circumscribing  ∃x.P(x) yields  ∃!x.P(x).
C00006 00004	"reiter%ubc"@csnet-Relay
C00009 00005	(wipe-out)
C00010 ENDMK
C⊗;
reiter[w84,jmc]		A proof for Reiter
(proof reiter)
(axiom |∃x.P x|)
(axiom |∀P1.(∃x.P1 x) ∧ (∀x.P1 x ⊃ P x) ⊃ (∀x.P x ⊃ P1 x)|)
(define a |P a| 1)
(ue (P1 |λx.x=a|) 2)
(der |∀x.x=a ⊃ p x| 3)
(trw |∀x.(p x ⊃ x = a)| 4 5)
(trw |∀x1 x2.p x1 ∧ p x2 ⊃ x1 = x2| (use 6 mode: exact))
(trw |∃!x.p x| 1 6 7 (open unique))
(show)

(cancel)
(axiom |(∃x.P x) ∧ (∀P1.(∃x.P1 x) ∧ (∀x.P1 x ⊃ P x) ⊃ (∀x.P x ⊃ P1 x))|)
(define a |P a| 1)
(ue (P1 |λx.x=a|) 1)
(der |∀x.x=a ⊃ p x| 2)
(trw |∀x.(p x ⊃ x = a)| 3 4)
(trw |∀x1 x2.p x1 ∧ p x2 ⊃ x1 = x2| (use 5 mode: exact))
(trw |∃!x.p x| 1 5 6 (open unique))
Here is an EKL proof that circumscribing  ∃x.P(x) yields  ∃!x.P(x).
Actually ∃! is not built in to EKL and has to be defined as a new
BINDOP.  Jussi Ketonen did this, and the present proof was preceded
by the proof involving the definition of the second order predicate
UNIQUE  and its use to give the properties of  ∃!.

Here is the EKL proof.  Where there are two lines, the first is the
command typed by the user (me), and the second is the formula proved.

1. (AXIOM |(∃X.P(X))∧(∀P1.(∃X.P1(X))∧(∀X.P1(X)⊃P(X))⊃(∀X.P(X)⊃P1(X)))|)
This is the circumscription of ∃x.P(x).  EKL doesn't have a circumscription
command yet, so we have to make it an axiom.

2. (DEFINE A |P(A)| (USE 1))
This is essentially an existential instantiation.

3. (UE ((P1.|λX.X=A|)) 1 NIL)
(∃X.P(X))∧((∀X.X=A⊃P(X))⊃(∀X.P(X)⊃X=A))
Making the right substitution in the circumscription formula.

4. (DERIVE |∀X.X=A⊃P(X)| (2) NIL)
∀X.X=A⊃P(X)
We need this as an explicit premiss, it seems, although I had hoped
to get by with a reference to the definition (2) in the next step.

5. (TRW |∀X.P(X)⊃X=A| ((USE 3) (USE 4)))
∀X.P(X)⊃X=A
Now we've got the conclusion of the circumscription.

6. (TRW |∀X1 X2.P(X1)∧P(X2)⊃X1=X2| (USE 5 MODE: EXACT))
∀X1 X2.P(X1)∧P(X2)⊃X1=X2
EKL requires that this be derived from  5, although one could hope that
it would be able to use 5 instead in the next step.

7. (TRW |∃! X.(P(X))| ((USE 1) (USE 5) (USE 6) (OPEN UNIQUE)))
∃! X.(P(X))
This is the answer.
"reiter%ubc"@csnet-Relay
circumscription sometimes works
Your proof about circumscribing equality looks correct to me, though
I want to ponder it further.  However, circumscribing  EX X.P(X) does
lead to E! X.P(X)  as the following  EKL proof shows.  EKL is Jussi
Ketonen's interactive theorem prover.  The only part that may require
explanation is the use of DEFINE in step 3.  This rule of EKL allows
one, given a proof of existence of an object satisfying given conditions,
allows one to define a new symbol as representing such an object.  It's
the way we do existential instantiation in EKL.

Incidentally, I have been challenged to give examples of the practical or
AI utility of circumscription in the case where it leads to a disjunction.
Do you have good examples from databases?  My interlocutor grumbles about
the example of the employer in Vancouver and the wife in Toronto on the
grounds that he personally wouldn't want to draw any conclusion at all
about the person's city of residence and is backed up by his psychologist.

1. (AXIOM |EX X.P(X)|)

2. (AXIOM
     |ALL P1.(EX X.P1(X))&(ALL X.P1(X) IMP P(X)) IMP (ALL X.P(X) IMP P1(X))|)

3. (DEFINE A |P(A)| (USE 1))

4. (UE ((P1.|LAMBDA X.X=A|)) 2 (OPEN A))
(ALL X.X=A IMP P(X)) IMP (ALL X.P(X) IMP X=A)

5. (DERIVE |ALL X.X=A IMP P(X)| (3) NIL)
ALL X.X=A IMP P(X)

6. (TRW |ALL X.P(X) IMP X=A| ((USE 4) (USE 5)))
ALL X.P(X) IMP X=A

7. 
(wipe-out)
(decl phi |ground⊗ground → truthval|)
(decl t |(ground⊗ground → truthval) → truthval|)
(axiom |∀phi.t(phi) ⊃ ∀x.phi(x,x))
(axiom |∀x1 x2.equal(x1,x2) ≡ x1 = x2|)
This seems unneeded for the time being.  Reiter's formalism is clear enough.